<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Multiset: Insertion Sort With Multisets</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/vfa.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 3: 函数式算法验证</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Multiset<span class="subtitle">Insertion Sort With Multisets</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 We have seen how to specify algorithms on "collections", such as
    sorting algorithms, using permutations.  Instead of using
    permutations, another way to specify these algorithms is to use
    multisets.  A _set_ of values is like a list with no repeats where
    the order does not matter.  A _multiset_ is like a list, possibly
    with repeats, where the order does not matter.  One simple
    representation of a multiset is a function from values to <span class="inlinecode"><span class="id" type="var">nat</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Strings.String</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">VFA</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Perm</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">VFA</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="keyword">Sort</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">FunctionalExtensionality</span>.<br/>
</div>

<div class="doc">
In this chapter we will be using natural numbers for two different
    purposes: the values in the lists that we sort, and the
    multiplicity (number of times occurring) of those values.  To keep
    things straight, we'll use the <span class="inlinecode"><span class="id" type="var">value</span></span> type for values, and <span class="inlinecode"><span class="id" type="var">nat</span></span>
    for multiplicities. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">value</span> := <span class="id" type="var">nat</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">multiset</span> := <span class="id" type="var">value</span> → <span class="id" type="var">nat</span>.<br/>
</div>

<div class="doc">
Just like sets, multisets have operators for <span class="inlinecode"><span class="id" type="var">union</span></span>, for the
    <span class="inlinecode"><span class="id" type="var">empty</span></span> multiset, and the multiset with just a single element. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty</span> : <span class="id" type="var">multiset</span> :=<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ 0.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">union</span> (<span class="id" type="var">a</span> <span class="id" type="var">b</span> : <span class="id" type="var">multiset</span>) : <span class="id" type="var">multiset</span> :=<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">a</span> <span class="id" type="var">x</span> + <span class="id" type="var">b</span> <span class="id" type="var">x</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">singleton</span> (<span class="id" type="var">v</span>: <span class="id" type="var">value</span>) : <span class="id" type="var">multiset</span> :=<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> =? <span class="id" type="var">v</span> <span class="id" type="keyword">then</span> 1 <span class="id" type="keyword">else</span> 0.<br/>
</div>

<div class="doc">
<a name="lab37"></a><h4 class="section">练习：1 星, standard (union_assoc)</h4>
 Since multisets are represented as functions, to prove that one
    multiset equals another we must use the axiom of functional
    extensionality. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">union_assoc</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> : <span class="id" type="var">multiset</span>, <span class="comment">(*&nbsp;assoc&nbsp;stands&nbsp;for&nbsp;"associative"&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">union</span> <span class="id" type="var">a</span> (<span class="id" type="var">union</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>) = <span class="id" type="var">union</span> (<span class="id" type="var">union</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span>) <span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">extensionality</span> <span class="id" type="var">x</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab38"></a><h4 class="section">练习：1 星, standard (union_comm)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">union_comm</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">b</span> : <span class="id" type="var">multiset</span>,  <span class="comment">(*&nbsp;comm&nbsp;stands&nbsp;for&nbsp;"commutative"&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">union</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span> = <span class="id" type="var">union</span> <span class="id" type="var">b</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Remark on efficiency:  These multisets aren't very efficient.  If
  you wrote programs with them, the programs would run slowly. However,
  we're using them for _specifications_, not for _programs_.  Our
  multisets built with <span class="inlinecode"><span class="id" type="var">union</span></span> and <span class="inlinecode"><span class="id" type="var">singleton</span></span> will never really
  _execute_ on any large-scale inputs; they're only used in the proof
  of correctness of algorithms such as <span class="inlinecode"><span class="id" type="var">sort</span></span>.  Therefore, their
  inefficiency is not a problem. 
<div class="paragraph"> </div>

 Contents of a list, as a multiset: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">contents</span> (<span class="id" type="var">al</span>: <span class="id" type="var">list</span> <span class="id" type="var">value</span>) : <span class="id" type="var">multiset</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">al</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">a</span> :: <span class="id" type="var">bl</span> ⇒ <span class="id" type="var">union</span> (<span class="id" type="var">singleton</span> <span class="id" type="var">a</span>) (<span class="id" type="var">contents</span> <span class="id" type="var">bl</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">empty</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
Recall the insertion-sort program from <span class="inlinecode"><span class="id" type="var">Sort.v</span></span>.  Note that it
    handles lists with repeated elements just fine. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">sort_pi</span>: <span class="id" type="var">sort</span> [3;1;4;1;5;9;2;6;5;3;5] = [1;1;2;3;3;4;5;5;5;6;9].<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">sort_pi_same_contents</span>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">contents</span> (<span class="id" type="var">sort</span> [3;1;4;1;5;9;2;6;5;3;5]) = <span class="id" type="var">contents</span> [3;1;4;1;5;9;2;6;5;3;5].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">extensionality</span> <span class="id" type="var">x</span>.<br/>
<span class="id" type="tactic">do</span> 10 (<span class="id" type="tactic">destruct</span> <span class="id" type="var">x</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Why&nbsp;does&nbsp;this&nbsp;work?&nbsp;Try&nbsp;it&nbsp;step&nbsp;by&nbsp;step,&nbsp;without&nbsp;<span class="inlinecode"><span class="id" type="tactic">do</span></span> <span class="inlinecode">10</span>&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab39"></a><h1 class="section">Correctness</h1>

<div class="paragraph"> </div>

 A sorting algorithm must rearrange the elements into a list that
    is totally ordered.  But let's say that a different way: the
    algorithm must produce a list _with the same multiset of values_,
    and this list must be totally ordered. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">is_a_sorting_algorithm'</span> (<span class="id" type="var">f</span>: <span class="id" type="var">list</span> <span class="id" type="var">nat</span> → <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">al</span>, <span class="id" type="var">contents</span> <span class="id" type="var">al</span> = <span class="id" type="var">contents</span> (<span class="id" type="var">f</span> <span class="id" type="var">al</span>) ∧ <span class="id" type="var">sorted</span> (<span class="id" type="var">f</span> <span class="id" type="var">al</span>).<br/>
</div>

<div class="doc">
<a name="lab40"></a><h4 class="section">练习：3 星, standard (insert_contents)</h4>
 First, prove the auxiliary lemma <span class="inlinecode"><span class="id" type="var">insert_contents</span></span>, which will be
    useful for proving <span class="inlinecode"><span class="id" type="var">sort_contents</span></span> below.  Your proof will be by
    induction.  You do not need to use <span class="inlinecode"><span class="id" type="tactic">extensionality</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">insert_contents</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">l</span>, <span class="id" type="var">contents</span> (<span class="id" type="var">x</span>::<span class="id" type="var">l</span>) = <span class="id" type="var">contents</span> (<span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab41"></a><h4 class="section">练习：3 星, standard (sort_contents)</h4>
 Now prove that sort preserves contents. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">sort_contents</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>, <span class="id" type="var">contents</span> <span class="id" type="var">l</span> = <span class="id" type="var">contents</span> (<span class="id" type="var">sort</span> <span class="id" type="var">l</span>).<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Now we wrap it all up.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">insertion_sort_correct</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">is_a_sorting_algorithm'</span> <span class="id" type="var">sort</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">split</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">sort_contents</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">sort_sorted</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab42"></a><h4 class="section">练习：1 星, standard (permutations_vs_multiset)</h4>
 Compare your proofs of <span class="inlinecode"><span class="id" type="var">insert_perm</span>,</span> <span class="inlinecode"><span class="id" type="var">sort_perm</span></span> with your proofs
    of <span class="inlinecode"><span class="id" type="var">insert_contents</span>,</span> <span class="inlinecode"><span class="id" type="var">sort_contents</span></span>.  Which proofs are simpler?

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> easier with permutations,

</li>
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> easier with multisets

</li>
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> about the same.

</li>
</ul>

<div class="paragraph"> </div>

   Regardless of "difficulty", which do you prefer / find easier to
   think about?

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> permutations or

</li>
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> multisets

</li>
</ul>

<div class="paragraph"> </div>

   Put an X in one box in each list. 
</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_permutations_vs_multiset</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab43"></a><h1 class="section">Permutations and Multisets</h1>

<div class="paragraph"> </div>

 The two specifications of insertion sort are equivalent.  One
    reason is that permutations and multisets are closely related.
    We're going to prove:

<div class="paragraph"> </div>

       <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span> <span class="inlinecode">↔</span> <span class="inlinecode"><span class="id" type="var">contents</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">contents</span></span> <span class="inlinecode"><span class="id" type="var">bl</span>.</span> 
<div class="paragraph"> </div>

<a name="lab44"></a><h4 class="section">练习：3 星, standard (perm_contents)</h4>
 The forward direction is easy, by induction on the evidence for
    <span class="inlinecode"><span class="id" type="var">Permutation</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">perm_contents</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">al</span> <span class="id" type="var">bl</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">Permutation</span> <span class="id" type="var">al</span> <span class="id" type="var">bl</span> → <span class="id" type="var">contents</span> <span class="id" type="var">al</span> = <span class="id" type="var">contents</span> <span class="id" type="var">bl</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The other direction,
    <span class="inlinecode"><span class="id" type="var">contents</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">contents</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span>,
    is surprisingly difficult.  (Or maybe there's an easy way
    that I didn't find.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">list_delete</span> (<span class="id" type="var">al</span>: <span class="id" type="var">list</span> <span class="id" type="var">value</span>) (<span class="id" type="var">v</span>: <span class="id" type="var">value</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">al</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span>::<span class="id" type="var">bl</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> =? <span class="id" type="var">v</span> <span class="id" type="keyword">then</span> <span class="id" type="var">bl</span> <span class="id" type="keyword">else</span> <span class="id" type="var">x</span> :: <span class="id" type="var">list_delete</span> <span class="id" type="var">bl</span> <span class="id" type="var">v</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">nil</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">multiset_delete</span> (<span class="id" type="var">m</span>: <span class="id" type="var">multiset</span>) (<span class="id" type="var">v</span>: <span class="id" type="var">value</span>) :=<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> =? <span class="id" type="var">v</span> <span class="id" type="keyword">then</span> <span class="id" type="var">pred</span>(<span class="id" type="var">m</span> <span class="id" type="var">x</span>) <span class="id" type="keyword">else</span> <span class="id" type="var">m</span> <span class="id" type="var">x</span>.<br/>
</div>

<div class="doc">
<a name="lab45"></a><h4 class="section">练习：3 星, standard (delete_contents)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">delete_contents</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">v</span> <span class="id" type="var">al</span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">contents</span> (<span class="id" type="var">list_delete</span> <span class="id" type="var">al</span> <span class="id" type="var">v</span>) = <span class="id" type="var">multiset_delete</span> (<span class="id" type="var">contents</span> <span class="id" type="var">al</span>) <span class="id" type="var">v</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">extensionality</span> <span class="id" type="var">x</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">al</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">empty</span>, <span class="id" type="var">multiset_delete</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">x</span> =? <span class="id" type="var">v</span>); <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">a</span> =? <span class="id" type="var">v</span>).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab46"></a><h4 class="section">练习：2 星, standard (contents_perm_aux)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">contents_perm_aux</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">v</span> <span class="id" type="var">b</span>, <span class="id" type="var">empty</span> = <span class="id" type="var">union</span> (<span class="id" type="var">singleton</span> <span class="id" type="var">v</span>) <span class="id" type="var">b</span> → <span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab47"></a><h4 class="section">练习：2 星, standard (contents_in)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">contents_in</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span>: <span class="id" type="var">value</span>) (<span class="id" type="var">bl</span>: <span class="id" type="var">list</span> <span class="id" type="var">value</span>) , <span class="id" type="var">contents</span> <span class="id" type="var">bl</span> <span class="id" type="var">a</span> &gt; 0 → <span class="id" type="var">In</span> <span class="id" type="var">a</span> <span class="id" type="var">bl</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab48"></a><h4 class="section">练习：2 星, standard (in_perm_delete)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">in_perm_delete</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">bl</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">a</span> <span class="id" type="var">bl</span> → <span class="id" type="var">Permutation</span> (<span class="id" type="var">a</span> :: <span class="id" type="var">list_delete</span> <span class="id" type="var">bl</span> <span class="id" type="var">a</span>) <span class="id" type="var">bl</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab49"></a><h4 class="section">练习：4 星, standard (contents_perm)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">contents_perm</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">al</span> <span class="id" type="var">bl</span>, <span class="id" type="var">contents</span> <span class="id" type="var">al</span> = <span class="id" type="var">contents</span> <span class="id" type="var">bl</span> → <span class="id" type="var">Permutation</span> <span class="id" type="var">al</span> <span class="id" type="var">bl</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">al</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">bl</span>; <span class="id" type="tactic">intro</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">contradiction</span> (<span class="id" type="var">contents_perm_aux</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">H</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">symmetry</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">contradiction</span> (<span class="id" type="var">contents_perm_aux</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">H</span>).<br/>
&nbsp;&nbsp;<span class="id" type="var">specialize</span> (<span class="id" type="var">IHal</span> (<span class="id" type="var">list_delete</span> (<span class="id" type="var">v</span> :: <span class="id" type="var">bl</span>) <span class="id" type="var">a</span>)).<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">v</span>::<span class="id" type="var">bl</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">cl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">clear</span> <span class="id" type="var">v</span> <span class="id" type="var">bl</span> <span class="id" type="var">Heqcl</span>.<br/>
</div>

<div class="doc">
From this point on, you don't need induction.
    Use the lemmas <span class="inlinecode"><span class="id" type="var">perm_trans</span></span>, <span class="inlinecode"><span class="id" type="var">delete_contents</span></span>,
     <span class="inlinecode"><span class="id" type="var">in_perm_delete</span></span>, <span class="inlinecode"><span class="id" type="var">contents_in</span></span>.   At _certain points_
     you'll need to unfold the definitions of
     <span class="inlinecode"><span class="id" type="var">multiset_delete</span></span>, <span class="inlinecode"><span class="id" type="var">union</span></span>, <span class="inlinecode"><span class="id" type="var">singleton</span></span>. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab50"></a><h1 class="section">The Main Theorem: Equivalence of Multisets and Permutations</h1>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">same_contents_iff_perm</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">al</span> <span class="id" type="var">bl</span>, <span class="id" type="var">contents</span> <span class="id" type="var">al</span> = <span class="id" type="var">contents</span> <span class="id" type="var">bl</span> ↔ <span class="id" type="var">Permutation</span> <span class="id" type="var">al</span> <span class="id" type="var">bl</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">split</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">contents_perm</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">perm_contents</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Therefore, it doesn't matter whether you prove your sorting
    algorithm using the Permutations method or the multiset method. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Corollary</span> <span class="id" type="var">sort_specifications_equivalent</span>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">sort</span>, <span class="id" type="var">is_a_sorting_algorithm</span> <span class="id" type="var">sort</span> ↔  <span class="id" type="var">is_a_sorting_algorithm'</span> <span class="id" type="var">sort</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">is_a_sorting_algorithm</span>, <span class="id" type="var">is_a_sorting_algorithm'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span>;<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">H</span> <span class="id" type="var">al</span>); <span class="id" type="tactic">split</span>; <span class="id" type="tactic">auto</span>;<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">same_contents_iff_perm</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:17:35&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>